(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const r0 Real)
(declare-const r2 Real)
(declare-const r5 Real)
(declare-const r8 Real)
(declare-const r9 Real)
(declare-const r11 Real)
(declare-const v6 Bool)
(declare-const r12 Real)
(declare-const r13 Real)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const r14 Real)
(declare-const v13 Bool)
(declare-const v14 Bool)
(assert (or v8 v8 v10 (=> (distinct r2 0.5763 2898892783.0) v8) v8 v2 v10 v2 (<= (/ 981223.0 r9) 0.5763 r11)))
(assert (or (<= (/ 981223.0 r9) 0.5763 r11) v2 v5))
(assert (or v5 v10))
(assert (or (=> (distinct r2 0.5763 2898892783.0) v8) (=> (distinct r2 0.5763 2898892783.0) v8) v10))
(assert (or (=> (distinct r2 0.5763 2898892783.0) v8) v10 v8 (and v7 v6 v0 (< 2898892783.0 5.8423058 71443772.0)) v5))
(assert (or (=> (distinct r2 0.5763 2898892783.0) v8) v2 v2 v10))
(assert (or v8 (<= (/ 981223.0 r9) 0.5763 r11) v5))
(check-sat)
